$\forall$${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $a$, $b$:msg{-}spec(${\it ds}$;${\it da}$). $a$ $\oplus$ $b$ $\in$ msg{-}spec(${\it ds}$;${\it da}$)